$\forall$$A$, $B$, $C$, $D$:Type.  $A$ $\sim$ $B$ $\Rightarrow$ ($C$ = $D$) $\Rightarrow$  :$A$ $\times$ $C$ $\sim$ :$B$ $\times$ $D$